Inference at * 1 1 2 1 
Iof proof for Lemma comp nat ind a:



1. P : {k}
2. i:. (j:. (j < i)  P(j))  P(i)
3. s : 
4. t:. (t < s)  P(t)
  P(s) 

latex

 by (% done % ((((((BHyp 2) 
CollapseTHENM (RepD))) 
CollapseTHENM (BHyp 4))) 
CollapseTHEN (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 3:n)) (first_tok :t) inil_term)))) 

latex

C.

Definitions	t  T, P  Q, x:A. B(x), ,
Lemmas	nat wf